1 /-
2 Copyright (c) 2019 Amelia Livingston. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Amelia Livingston
5 -/
6
7 import group_theory.congruence
src └─────────────────────┘
8 import algebra.associated
src └────────────────┘
9 import tactic.abel
src └─────────┘
10
11 /-
12
13 # Localizations of commutative monoids
14
15 The standard congruence relation (an equivalence relation preserving a binary operation) used to
16 define commutative ring localizations does not rely on the ring's addition. For a commutative
17 monoid `X` and submonoid `Y`, this relation can be expressed as
18 `∀ (x₁, y₁) (x₂, y₂) : X × Y, x ∼ y ↔ ∃ c ∈ Y, c * x₁ * y₂ = c * x₂ * y₁`, or, equivalently, as the
19 unique congruence relation `r` on `X × Y` such that for any other congruence relation `r'` on
20 `X × Y` where for all `y ∈ Y`, `(1, 1) ∼ (y, y)` under `r'`, we have that `(x₁, y₁) ∼ (x₂, y₂)` by
21 `r'` implies `(x₁, y₁) ∼ (x₂, y₂)` by `r`.
22
23 The first half of the file contains basic lemmas about the localization of `X` at `Y` - the
24 commutative monoid we get when we quotient `X × Y` by this congruence relation - and some
25 associated monoid homomorphisms: the quotient map, `localization.mk`, the quotient map restricted
26 to `X × {1}`, `localization.monoid.of`, and the quotient map restricted to `Y × {1}`,
27 `localization.monoid.to_units`, whose image is contained in the unit group of the localization of
28 `X` at `Y`.
29 Subsequently we prove basic lemmas about `localization.monoid.lift'` (constructive version) and
30 `localization.monoid.lift` (classical version): given a `comm_monoid` homomorphism `f : X → Z`
31 mapping elements of a submonoid `Y` to invertible elements of `Z`, these are the homomorphism
32 from the localization of `X` at `Y` sending `⟦(x, y)⟧` to `f(x) * f(y)⁻¹`. If `f(Y)` is contained
33 in a submonoid `W` of `Z`, we can also define the map from the localization of `X` at `Y`
34 to the localization of `Z` at `W` induced by `(of W) ∘ f`, where `of W` is the natural map from `Z`
35 to the localization of `Z` at `W`. This is called `localization.monoid.map`.
36
37 ## Implementation notes
38
39 The infimum form of the localization congruence relation is chosen as 'canonical' here, since it
40 shortens many proofs.
41
42 The `private def` `r'.rel` and the lemmas `r'.add, r'.transitive` are to enable the use of the
43 `abel` tactic for both the additive and multiplicative proofs that the 'usual' localization
44 congruence relation is a congruence relation.
45
46 There is only a multiplicative version for any lemma or definition relying on a unit group of a
47 `comm_monoid`; additive versions would require additive unit groups.
48
49 ## Tags
50 localization, monoid localization, quotient monoid, congruence relation
51
52 -/
53 variables {X : Type*}
54
55 namespace submonoid
56
57 /-- The congruence relation on `X × Y`, `X` a `comm_monoid` and `Y` a submonoid of `X`, whose
58 quotient is the localization of `X` at `Y`, defined as the unique congruence relation on
59 `X × Y` such that for any other congruence relation `s` on `X × Y` where for all `y ∈ Y`,
60 `(1, 1) ∼ (y, y)` under `s`, we have that `(x₁, y₁) ∼ (x₂, y₂)` by `s` implies
61 `(x₁, y₁) ∼ (x₂, y₂)` by `r`. -/
62 @[to_additive "The congruence relation on `X × Y`, `X` an `add_comm_monoid` and `Y` an `add_submonoid` of `X`, whose quotient is the localization of `X` at `Y`, defined as the unique congruence relation on `X × Y` such that for any other congruence relation `s` on `X × Y` where for all `y ∈ Y`, `(0, 0) ∼ (y, y)` under `s`, we have that `(x₁, y₁) ∼ (x₂, y₂)` by `s` implies `(x₁, y₁) ∼ (x₂, y₂)` by `r`."]
doc └─────────┘
63 def r [comm_monoid X] (Y : submonoid X) : con (X × Y) :=
id └─────────┘ ┴ └───────┘ ┴ └─┘ ┴ ┴ ┴
src └─────────┘ └───────┘ └─┘ ┴
typ └─────────┘ ┴ └───────┘ ┴ └─┘ ┴ ┴ ┴
doc └───────┘ └─┘
64 lattice.Inf {c | ∀ y : Y, c 1 (y, y)}
id └─────────┘ ┴┴ ┴ ┴ ┴┴ ┴
src └─────────┘ ┴ ┴
typ └─────────┘ ┴┴ ┴ ┴ ┴┴ ┴
doc └─────────┘
65
66 end submonoid
67
68 namespace add_submonoid
69
70 variables [add_comm_monoid X]
id └─────────────┘
src └─────────────┘
typ └─────────────┘
71
72 /-- An alternate form of the `add_monoid` localization relation, stated here for readability of the
73 next few lemmas. -/
74 private def r'.rel (Y : add_submonoid X) (a b : X × Y) :=
id └───────────┘ ┴ ┴ ┴ ┴
src └───────────┘ ┴
typ └───────────┘ ┴ ┴ ┴ ┴
doc └───────────┘
75 ∃ c : Y, (c : X) + (a.1 + b.2) = c + (b.1 + a.2)
id ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
76
77 lemma r'.transitive {Y : add_submonoid X} : transitive (r'.rel Y) :=
id └───────────┘ ┴ └────────┘ └────┘ ┴
src └───────────┘ └────────┘ └────┘
typ └───────────┘ ┴ └────────┘ └────┘ ┴
doc └───────────┘ └────┘
78 λ a b c ⟨m, hm⟩ ⟨n, hn⟩, ⟨n + m + b.2,
id ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴┴
79 calc
80 ↑n + ↑m + ↑b.2 + (a.1 + ↑c.2)
id ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴ ┴ ┴┴┴
81 = ↑n + (↑m + (b.1 + ↑a.2)) + ↑c.2 : by rw ←hm; abel
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴ └┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └────
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴ └──┘└┘ └────
doc └──┘ └────
txt └──┘ └────
par └──┘ └────
pid └┘ └
st └─────────────
82 ... = ↑m + (↑n + (c.1 + ↑b.2)) + ↑a.2 : by rw ←hn; abel
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴ └┘
src ─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └────
typ ─┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴ └──┘└┘ └────
doc ─┘ └──┘ └────
txt ─┘ └──┘ └────
par ─┘ └──┘ └────
pid ─┘ └┘ └
st ─┘ └─────────────
83 ... = ↑n + ↑m + ↑b.2 + (c.1 + ↑a.2) : by abel⟩
id ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴ ┴ ┴┴┴
src ─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
typ ─┘ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴ ┴ ┴┴┴ └──┘
doc ─┘ └──┘
txt ─┘ └──┘
par ─┘ └──┘
pid ─┘
st ─┘ └───┘
84
85 lemma r'.add {Y : add_submonoid X} {a b c d} :
id └───────────┘ ┴
src └───────────┘
typ └───────────┘ ┴
doc └───────────┘
86 r'.rel Y a b → r'.rel Y c d → r'.rel Y (a + c) (b + d) :=
id └────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────┘ └────┘ └────┘ ┴ ┴
typ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └────┘ └────┘ └────┘
87 λ ⟨m, hm⟩ ⟨n, hn⟩, ⟨m + n,
id ┴┴ ┴┴ ┴
src ┴
typ ┴┴ ┴┴ ┴
88 calc
89 ↑m + ↑n + (a.1 + c.1 + (↑b.2 + ↑d.2))
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
90 = ↑n + c.1 + (↑m + (b.1 + ↑a.2)) + ↑d.2 : by rw ←hm; abel
id ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴ └┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └────
typ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴ └──┘└┘ └────
doc └──┘ └────
txt └──┘ └────
par └──┘ └────
pid └┘ └
st └─────────────
91 ... = (↑m + (b.1 + ↑a.2)) + (↑n + (d.1 + ↑c.2)) : by rw ←hn; abel
id ┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴┴ └┘
src ─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └────
typ ─┘ ┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴┴ └──┘└┘ └────
doc ─┘ └──┘ └────
txt ─┘ └──┘ └────
par ─┘ └──┘ └────
pid ─┘ └┘ └
st ─┘ └─────────────
92 ... = ↑m + ↑n + (b.1 + d.1 + (↑a.2 + ↑c.2)) : by abel⟩
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴
src ─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
typ ─┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴┴┴ └──┘
doc ─┘ └──┘
txt ─┘ └──┘
par ─┘ └──┘
pid ─┘
st ─┘ └───┘
93
94 /-- An alternate form of the congruence relation on `X × Y`, `X` an `add_comm_monoid` and `Y` an
95 `add_submonoid` of `X`, whose quotient is the localization of `X` at `Y`. Its equivalence to
96 `r` can be useful for proofs. -/
97 def r' (Y : add_submonoid X) : add_con (X × Y) :=
id └───────────┘ ┴ └─────┘ ┴ ┴ ┴
src └───────────┘ └─────┘ ┴
typ └───────────┘ ┴ └─────┘ ┴ ┴ ┴
doc └───────────┘ └─────┘
98 { r := λ a b, ∃ c : Y, (c : X) + (a.1 + b.2) = c + (b.1 + a.2),
id ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
99 iseqv := ⟨λ _, ⟨0, rfl⟩, λ _ _ ⟨c, hc⟩, ⟨c, hc.symm⟩, r'.transitive⟩,
id ┴ └─┘ ┴ ┴ ┴┴ └┘ └───┘ └───────────┘
src └─┘ └───┘ └───────────┘
typ ┴ └─┘ ┴ ┴ ┴┴ └┘ └───┘ └───────────┘
100 add' := λ a b c d, r'.add }
id ┴ ┴ ┴ ┴ └────┘
src └────┘
typ ┴ ┴ ┴ ┴ └────┘
101
102 end add_submonoid
103
104 variables [comm_monoid X] (Y : submonoid X) {Z : Type*} [comm_monoid Z]
id └─────────┘ └───────┘ └─────────┘
src └─────────┘ └───────┘ └─────────┘
typ └─────────┘ └───────┘ └─────────┘
doc └───────┘
st └───────┘
105
106 namespace submonoid
107
108 /-- An alternate form of the congruence relation on `X × Y`, `X` a `comm_monoid` and `Y` a
109 submonoid of `X`, whose quotient is the localization of `X` at `Y`. Its equivalence to `r` can
110 be useful for proofs. -/
111 def r' : con (X × Y) :=
id └─┘ ┴ ┴ ┴
src └─┘ ┴
typ └─┘ ┴ ┴ ┴
doc └─┘
112 { r := λ a b, ∃ c : Y, (c : X) * (a.1 * b.2) = c * (b.1 * a.2),
id ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴┴
113 iseqv := ⟨λ _, ⟨1, rfl⟩, λ _ _ ⟨c, hc⟩, ⟨c, hc.symm⟩,
id ┴ └─┘ ┴ ┴ ┴┴ └┘ └───┘
src └─┘ └───┘
typ ┴ └─┘ ┴ ┴ ┴┴ └┘ └───┘
114 @add_submonoid.r'.transitive (additive X) _ $ submonoid.to_add_submonoid Y⟩,
id └─────────────────────────┘ └──────┘ ┴ └────────────────────────┘ ┴
src └─────────────────────────┘ └──────┘ └────────────────────────┘
typ └─────────────────────────┘ └──────┘ ┴ └────────────────────────┘ ┴
doc └────────────────────────┘
115 mul' := @add_submonoid.r'.add (additive X) _ $ submonoid.to_add_submonoid Y }
id └──────────────────┘ └──────┘ ┴ └────────────────────────┘ ┴
src └──────────────────┘ └──────┘ └────────────────────────┘
typ └──────────────────┘ └──────┘ ┴ └────────────────────────┘ ┴
doc └────────────────────────┘
116
117 attribute [to_additive add_submonoid.r'] submonoid.r'
id └──────────┘
src └──────────┘
typ └──────────┘
doc └─────────┘ └──────────┘
118
119 /-- The congruence relation used to localize a `comm_monoid` at a submonoid can be expressed
120 equivalently as an infimum (see `submonoid.r`) or explicitly (see `submonoid.r'`). -/
121 @[to_additive "The additive congruence relation used to localize an `add_comm_monoid` at a submonoid can be expressed equivalently as an infimum (see `add_submonoid.r`) or explicitly (see `add_submonoid.r'`)."]
doc └─────────┘
122 theorem r_eq_r' : Y.r = Y.r' :=
id ┴└┘ ┴ ┴└─┘
src └┘ ┴ └─┘
typ ┴└┘ ┴ ┴└─┘
doc └┘ └─┘
123 le_antisymm (lattice.Inf_le $ λ _, ⟨1, by norm_num⟩) $
id └─────────┘ └────────────┘ ┴
src └─────────┘ └────────────┘ └──────┘
typ └─────────┘ └────────────┘ ┴ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
st └───────┘
124 lattice.le_Inf $ λ b H x y ⟨t, ht⟩,
id └────────────┘ ┴ ┴ ┴ ┴ ┴
src └────────────┘
typ └────────────┘ ┴ ┴ ┴ ┴ ┴
125 begin
st └─────
126 rw [show x = (1 * x.1, 1 * x.2), by simp, show y = (1 * y.1, 1 * y.2), by simp],
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴┴┴┴└┘┴┴ └────┘ ┴ └──────┘└──┘└┘ ┴ ┴ ┴┴└┘ ┴ └────┘ ┴ └──────┘└──┘┴
typ └──┘ ┴ ┴┴┴┴└┘┴┴ └────┘ ┴┴└──────┘└──┘└┘ ┴ ┴┴┴┴└┘ ┴ └────┘ ┴┴└──────┘└──┘┴
doc └──┘ ┴ ┴ ┴ └┘ ┴ └────┘ ┴ └──────┘└──┘└┘ ┴ ┴ ┴ └┘ ┴ └────┘ ┴ └──────┘└──┘┴
txt └──┘ ┴ ┴ ┴ └┘ ┴ └────┘ ┴ └──────┘└──┘└┘ ┴ ┴ ┴ └┘ ┴ └────┘ ┴ └──────┘└──┘┴
par └──┘ ┴ ┴ ┴ └┘ ┴ └────┘ ┴ └──────┘└──┘└┘ ┴ ┴ ┴ └┘ ┴ └────┘ ┴ └──────┘└──┘┴
pid └┘ ┴ ┴ ┴ └┘ ┴ └────┘ ┴ └────────────┘ ┴ ┴ ┴ └┘ ┴ └────┘ ┴ └───────────┘
st ────────────────────────────────────────┘└───┘└───────────────────────────────┘└───┘└──
127 refine b.trans
id └─────┘
src └─────┘└─────┘└
typ └─────┘└─────┘└
doc └─────┘└─────┘└
txt └─────┘ └
par └─────┘ └
pid ┴ └
st ─────────────────────
128 (show b _ ((t : X) * y.2 * x.1, t * y.2 * x.2), from
id ┴ ┴
src ──────┘ ┴ └─┘ └─┘ └┘ ┴ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ └─────────
typ ──────┘ ┴┴└─┘ └─┘┴└┘ ┴ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ └─────────
doc ──────┘ ┴ └─┘ └─┘ └┘ ┴ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ └─────────
txt ──────┘ ┴ └─┘ └─┘ └┘ ┴ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ └─────────
par ──────┘ ┴ └─┘ └─┘ └┘ ┴ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ └─────────
pid ──────┘ ┴ └─┘ └─┘ └┘ ┴ └─┘ ┴ └──┘ ┴ ┴ └─┘ ┴ └─────────
st ────────────────────────────────────────────────────────────
129 b.mul (H (t * y.2)) $ b.refl (x.1, x.2)) _,
id └───┘ ┴ ┴ ┴ └────┘ ┴
src ────────┘└───┘┴ ┴ ┴ ┴ └───┘ ┴└────┘┴ └──┘ └────┘
typ ────────┘└───┘┴ ┴┴ ┴┴ ┴┴└───┘ ┴└────┘┴ └──┘┴└────┘
doc ────────┘└───┘┴ ┴ ┴ ┴ └───┘ ┴└────┘┴ └──┘ └────┘
txt ────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └──┘ └────┘
par ────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └──┘ └────┘
pid ────────┘ ┴ ┴ ┴ ┴ └───┘ ┴ ┴ └──┘ └────┘
st ──────────────────────────────────────────────────┘└─
130 rw [mul_assoc, mul_comm _ x.1, ht, mul_comm y.1, mul_assoc, mul_comm y.2,
id └───────┘ └──────┘ ┴ └┘ └──────┘ ┴ └───────┘ └──────┘ ┴
src └──┘└───────┘└┘└──────┘└─┘ └──┘ └┘└──────┘┴ └──┘└───────┘└┘└──────┘┴ └───
typ └──┘└───────┘└┘└──────┘└─┘┴└──┘└┘└┘└──────┘┴┴└──┘└───────┘└┘└──────┘┴┴└───
doc └──┘ └┘ └─┘ └──┘ └┘ ┴ └──┘ └┘ ┴ └───
txt └──┘ └┘ └─┘ └──┘ └┘ ┴ └──┘ └┘ ┴ └───
par └──┘ └┘ └─┘ └──┘ └┘ ┴ └──┘ └┘ ┴ └───
pid └┘ └┘ └─┘ └──┘ └┘ ┴ └──┘ └┘ ┴ └───
st ──────────────────┘└────────────┘└────┘└──────────┘└───────────┘└──────────┘└───
131 ←mul_assoc, ←mul_assoc],
id └───────┘ └───────┘
src ──────────┘└───────┘└─┘└───────┘┴
typ ──────────┘└───────┘└─┘└───────┘┴
doc ──────────┘ └─┘ ┴
txt ──────────┘ └─┘ ┴
par ──────────┘ └─┘ ┴
pid ──────────┘ └─┘ ┴
st ───────────────────┘└──────────┘└──
132 exact b.mul (b.symm $ H $ t * x.2) (b.refl (y.1, y.2))
id └───┘ └────┘ ┴ ┴ ┴ └────┘ ┴
src └────┘└───┘┴ └────┘┴ ┴ ┴ ┴ ┴ ┴ └──┘ └────┘┴ └──┘ └────
typ └────┘└───┘┴ └────┘┴ ┴┴┴ ┴┴┴ ┴┴└──┘ └────┘┴ └──┘┴└────
doc └────┘└───┘┴ └────┘┴ ┴ ┴ ┴ ┴ ┴ └──┘ └────┘┴ └──┘ └────
txt └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └──┘ └────
par └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └──┘ └────
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ └──┘ └──┘└
st ─────────────────────────────────────────────────────────────
133 end
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘└─┘
134
135 end submonoid
136
137 variables (X)
138
139 /-- The localization of a `comm_monoid` at one of its submonoids. -/
140 @[to_additive add_monoid_localization "The localization of an `add_comm_monoid` at one of its submonoids."]
doc └─────────┘
141 def monoid_localization := Y.r.quotient
id ┴└┘└───────┘
src └┘└───────┘
typ ┴└┘└───────┘
doc └┘└───────┘
142
143 variables {X Y}
144
145 namespace monoid_localization
146
147 /-- For all `y` in `Y`, a submonoid of a `comm_monoid` `X`, `(1, 1) ∼ (y, y)` under the relation
148 defining the localization of `X` at `Y`. -/
149 @[to_additive "For all `y` in `Y`, a submonoid of an `add_comm_monoid` `X`, `(0, 0) ∼ (y, y)` under the relation defining the localization of `X` at `Y`."]
doc └─────────┘
150 lemma one_rel (y : Y) : Y.r 1 (y, y) := by rw Y.r_eq_r'; use 1; norm_num
id ┴ ┴└┘ ┴┴ ┴
src └┘ ┴ └─┘ └───┘ └────────
typ ┴ ┴└┘ ┴┴ ┴ └─┘└───────┘ └───┘ └────────
doc └┘ └─┘ └───┘ └────────
txt └─┘ └───┘ └────────
par └─┘ └───┘ └────────
pid ┴ ┴┴ └
st └──────────────────────────────
151
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
152 /-- Given a `comm_monoid` `X` and submonoid `Y`, `mk` sends `x : X`, `y ∈ Y` to the equivalence
153 class of `(x, y)` in the localization of `X` at `Y`. -/
154 @[to_additive "Given an `add_comm_monoid` `X` and submonoid `Y`, `mk` sends `x : X`, `y ∈ Y` to the equivalence class of `(x, y)` in the localization of `X` at `Y`."]
doc └─────────┘
155 def mk (x : X) (y : Y) : monoid_localization X Y := Y.r.mk' (x, y)
id ┴ ┴ └─────────────────┘ ┴ ┴ ┴└┘└──┘ ┴┴ ┴
src └─────────────────┘ └┘└──┘ ┴
typ ┴ ┴ └─────────────────┘ ┴ ┴ ┴└┘└──┘ ┴┴ ┴
doc └─────────────────┘ └┘└──┘
156
157 @[elab_as_eliminator, to_additive]
doc └────────────────┘ └─────────┘
158 theorem ind {p : monoid_localization X Y → Prop}
id └─────────────────┘ ┴ ┴
src └─────────────────┘
typ └─────────────────┘ ┴ ┴
doc └─────────────────┘
159 (H : ∀ (y : X × Y), p (mk y.1 y.2)) (x) : p x :=
id ┴ ┴ ┴ ┴ └┘ ┴┴ ┴┴ ┴ ┴
src ┴ └┘ ┴ ┴
typ ┴ ┴ ┴ ┴ └┘ ┴┴ ┴┴ ┴ ┴
doc └┘
160 by rcases x; convert H x; exact prod.mk.eta.symm
id ┴ ┴ ┴ └──────────────┘
src └─────┘ └──────┘ ┴ └────┘└──────────────┘└
typ └─────┘┴ └──────┘┴┴┴ └────┘└──────────────┘└
doc └─────┘ └──────┘ ┴ └────┘ └
txt └─────┘ └──────┘ ┴ └────┘ └
par └─────┘ └──────┘ ┴ └────┘ └
pid ┴ ┴ ┴ ┴ └
st └──────────────────────────────────────────────
161
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
162 @[elab_as_eliminator, to_additive]
doc └────────────────┘ └─────────┘
163 theorem induction_on {p : monoid_localization X Y → Prop} (x)
id └─────────────────┘ ┴ ┴
src └─────────────────┘
typ └─────────────────┘ ┴ ┴
doc └─────────────────┘
164 (H : ∀ (y : X × Y), p (mk y.1 y.2)) : p x := ind H x
id ┴ ┴ ┴ ┴ └┘ ┴┴ ┴┴ ┴ ┴ └─┘ ┴ ┴
src ┴ └┘ ┴ ┴ └─┘
typ ┴ ┴ ┴ ┴ └┘ ┴┴ ┴┴ ┴ ┴ └─┘ ┴ ┴
doc └┘
165
166 @[to_additive] lemma exists_rep (x) : ∃ y : X × Y, mk y.1 y.2 = x :=
id ┴ ┴ ┴ ┴┴ └┘ ┴┴ ┴┴ ┴ ┴
src ┴ ┴ ┴ └┘ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴┴ └┘ ┴┴ ┴┴ ┴ ┴
doc └─────────┘ └┘
167 induction_on x $ λ y, ⟨y, rfl⟩
id └──────────┘ ┴ ┴ ┴ └─┘
src └──────────┘ └─┘
typ └──────────┘ ┴ ┴ ┴ └─┘
168
169 @[to_additive] instance : has_mul (monoid_localization X Y) := Y.r.has_mul
id └─────┘ └─────────────────┘ ┴ ┴ ┴└┘└──────┘
src └─────┘ └─────────────────┘ └┘└──────┘
typ └─────┘ └─────────────────┘ ┴ ┴ ┴└┘└──────┘
doc └─────────┘ └─────────────────┘ └┘└──────┘
170
171 @[to_additive] instance : comm_monoid (monoid_localization X Y) :=
id └─────────┘ └─────────────────┘ ┴ ┴
src └─────────┘ └─────────────────┘
typ └─────────┘ └─────────────────┘ ┴ ┴
doc └─────────┘ └─────────────────┘
172 Y.r.comm_monoid
id ┴└┘└──────────┘
src └┘└──────────┘
typ ┴└┘└──────────┘
doc └┘└──────────┘
173
174 @[to_additive] instance : inhabited (monoid_localization X Y) := ⟨1⟩
id └───────┘ └─────────────────┘ ┴ ┴
src └───────┘ └─────────────────┘
typ └───────┘ └─────────────────┘ ┴ ┴
doc └─────────┘ └─────────────────┘
175
176 @[to_additive] protected lemma eq {a₁ b₁} {a₂ b₂ : Y} :
id ┴
typ ┴
doc └─────────┘
177 mk a₁ a₂ = mk b₁ b₂ ↔ ∀ c : con (X × Y), (∀ y : Y, c 1 (y, y)) → c (a₁, a₂) (b₁, b₂) :=
id └┘ └┘ └┘ ┴ └┘ └┘ └┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴└┘ └┘ ┴└┘ └┘
src └┘ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ ┴
typ └┘ └┘ └┘ ┴ └┘ └┘ └┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴└┘ └┘ ┴└┘ └┘
doc └┘ └┘ └─┘
178 Y.r.eq.trans $ iff.rfl
id ┴└┘└─┘└────┘ └─────┘
src └┘└─┘└────┘ └─────┘
typ ┴└┘└─┘└────┘ └─────┘
doc └┘└─┘
179
180 @[to_additive] protected lemma eq' {a₁ b₁} {a₂ b₂ : Y} :
id ┴
typ ┴
doc └─────────┘
181 mk a₁ a₂ = mk b₁ b₂ ↔ ∃ c : Y, (c : X) * (a₁ * b₂) = c * (b₁ * a₂) :=
id └┘ └┘ └┘ ┴ └┘ └┘ └┘ ┴ ┴ ┴┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘
src └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └┘ └┘ └┘ ┴ └┘ └┘ └┘ ┴ ┴ ┴┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘
doc └┘ └┘
182 ⟨λ h, let ⟨w, hw⟩ := show Y.r' (a₁, a₂) (b₁, b₂), by rw [←Y.r_eq_r', ←con.eq]; exact h in ⟨w, hw⟩,
id ┴ └─┘ ┴ └┘ ┴└─┘ ┴└┘ └┘ ┴└┘ └┘ └────┘ ┴
src └─┘ ┴ ┴ └───┘ └─┘└────┘┴ └────┘ ┴
typ ┴ └─┘ ┴ └┘ ┴└─┘ ┴└┘ └┘ ┴└┘ └┘ └───┘└───────┘└─┘└────┘┴ └────┘┴┴
doc └─┘ └───┘ └─┘└────┘┴ └────┘ ┴
txt └───┘ └─┘ ┴ └────┘ ┴
par └───┘ └─┘ ┴ └────┘ ┴
pid └─┘ └─┘ ┴ ┴ ┴
st └─────────────┘└───────┘┴└────────┘
183 λ ⟨w, hw⟩, by erw [Y.r.eq, Y.r_eq_r']; exact ⟨w, hw⟩⟩
id ┴ ┴ └┘
src └───┘ └┘ ┴ └────┘ └┘ ┴
typ ┴ └───┘└────┘└┘└───────┘┴ └────┘ ┴└┘└┘┴
doc └───┘ └┘ ┴ └────┘ └┘ ┴
txt └───┘ └┘ ┴ └────┘ └┘ ┴
par └───┘ └┘ ┴ └────┘ └┘ ┴
pid └┘ └┘ ┴ ┴ └┘ ┴
st └──────────┘└─────────┘┴└─────────────┘
184
185 @[to_additive] lemma mk_eq_of_eq {a₁ b₁} {a₂ b₂ : Y} (h : (a₂ : X) * b₁ = b₂ * a₁) :
id ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘
src ┴ ┴ ┴
typ ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘
doc └─────────┘
186 mk a₁ a₂ = mk b₁ b₂ :=
id └┘ └┘ └┘ ┴ └┘ └┘ └┘
src └┘ ┴ └┘
typ └┘ └┘ └┘ ┴ └┘ └┘ └┘
doc └┘ └┘
187 monoid_localization.eq'.2 $ ⟨1, by rw [mul_comm b₁, h, mul_comm a₁]⟩
id └─────────────────────┘┴ └──────┘ └┘ ┴ └──────┘ └┘
src └─────────────────────┘┴ └──┘└──────┘┴ └┘ └┘└──────┘┴ ┴
typ └─────────────────────┘┴ └──┘└──────┘┴└┘└┘┴└┘└──────┘┴└┘┴
doc └──┘ ┴ └┘ └┘ ┴ ┴
txt └──┘ ┴ └┘ └┘ ┴ ┴
par └──┘ ┴ └┘ └┘ ┴ ┴
pid └┘ ┴ └┘ └┘ ┴ ┴
st └──────────────┘└─┘└───────────┘┴
188
189 @[simp, to_additive] lemma mk_self' (x : Y) : mk (x : X) x = 1 :=
id ┴ └┘ ┴ ┴ ┴ ┴
src └┘ ┴
typ ┴ └┘ ┴ ┴ ┴ ┴
doc └──┘ └─────────┘ └┘
190 monoid_localization.eq.2 $ λ c h, c.symm $ h x
id └────────────────────┘┴ ┴ ┴ ┴└───┘ ┴ ┴
src └────────────────────┘┴ └───┘
typ └────────────────────┘┴ ┴ ┴ ┴└───┘ ┴ ┴
doc └───┘
191
192 @[simp, to_additive] lemma mk_self {x} (hx : x ∈ Y) : mk x ⟨x, hx⟩ = 1 :=
id ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src ┴ └┘ ┴
typ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
doc └──┘ └─────────┘ └┘
193 mk_self' ⟨x, hx⟩
id └──────┘ ┴ └┘
src └──────┘
typ └──────┘ ┴ └┘
194
195 @[simp, to_additive] lemma mk_mul_mk (x y) (s t : Y) :
id ┴
typ ┴
doc └──┘ └─────────┘
196 mk x s * mk y t = mk (x * y) (s * t) := rfl
id └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
src └┘ ┴ └┘ ┴ └┘ ┴ ┴ └─┘
typ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘
doc └┘ └┘ └┘
197
198 /-- Definition of the function on the localization of a `comm_monoid` at a submonoid induced by a
199 function that is constant on the equivalence classes of the localization relation. -/
200 @[simp, to_additive "Definition of the function on the localization of an `add_comm_monoid` at an `add_submonoid` induced by a function that is constant on the equivalence classes of the localization relation."]
doc └──┘ └─────────┘
201 lemma lift_on_beta {β} (f : (X × Y) → β) (H : ∀ a b, Y.r a b → f a = f b) (x y) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴└┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴└┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘
202 con.lift_on (mk x y) f H = f (x, y) := rfl
id └─────────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └─┘
src └─────────┘ └┘ ┴ ┴ └─┘
typ └─────────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ └─┘
doc └─────────┘ └┘
203
204 /-- Natural homomorphism sending `x : X`, `X` a `comm_monoid`, to the equivalence class of
205 `(x, 1)` in the localization of `X` at a submonoid. For a `comm_ring` localization, this is
206 a ring homomorphism named `localization.of`. -/
207 @[to_additive "Natural homomorphism sending `x : X`, `X` an `add_comm_monoid`, to the equivalence class of `(x, 0)` in the localization of `X` at a submonoid."]
doc └─────────┘
208 def of (Y) : X →* monoid_localization X Y :=
id ┴ └┘ └─────────────────┘ ┴ ┴
src └┘ └─────────────────┘
typ ┴ └┘ └─────────────────┘ ┴ ┴
doc └┘ └─────────────────┘
209 Y.r.mk'.comp ⟨λ x, (x, 1), refl 1, λ _ _, by simp only [prod.mk_mul_mk, one_mul]⟩
id ┴└┘└──┘└───┘ ┴ ┴┴ └──┘ ┴ ┴ └────────────┘ └─────┘
src └┘└──┘└───┘ ┴ └──┘ └─────────┘└────────────┘└┘└─────┘┴
typ ┴└┘└──┘└───┘ ┴ ┴┴ └──┘ ┴ ┴ └─────────┘└────────────┘└┘└─────┘┴
doc └┘└──┘└───┘ └─────────┘ └┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st └──────────────────────────────────┘
210
211 @[to_additive] lemma of_ker_iff {x y} : con.ker (of Y) x y ↔ Y.r (x, 1) (y, 1) :=
id └─────┘ └┘ ┴ ┴ ┴ ┴ ┴└┘ ┴┴ ┴┴
src └─────┘ └┘ ┴ └┘ ┴ ┴
typ └─────┘ └┘ ┴ ┴ ┴ ┴ ┴└┘ ┴┴ ┴┴
doc └─────────┘ └─────┘ └┘ └┘
212 con.eq _
id └────┘
src └────┘
typ └────┘
doc └────┘
213
214 @[to_additive] lemma of_eq_mk (x) : of Y x = mk x 1 := rfl
id └┘ ┴ ┴ ┴ └┘ ┴ └─┘
src └┘ ┴ └┘ └─┘
typ └┘ ┴ ┴ ┴ └┘ ┴ └─┘
doc └─────────┘ └┘ └┘
215
216 @[simp, to_additive] lemma of_mul_mk (x y v) : of Y x * mk y v = mk (x * y) v :=
id └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
src └┘ ┴ └┘ ┴ └┘ ┴
typ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
doc └──┘ └─────────┘ └┘ └┘ └┘
217 by rw [of_eq_mk, mk_mul_mk, one_mul]
id └──────┘ └───────┘ └─────┘
src └──┘└──────┘└┘└───────┘└┘└─────┘└─
typ └──┘└──────┘└┘└───────┘└┘└─────┘└─
doc └──┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └─
par └──┘ └┘ └┘ └─
pid └┘ └┘ └┘ ┴└
st └───────────┘└─────────┘└───────┘┴└
218
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
219 @[to_additive] lemma mk_eq_mul_mk_one (x y) : mk x y = of Y x * mk 1 y :=
id └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴
src └┘ ┴ └┘ ┴ └┘
typ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴
doc └─────────┘ └┘ └┘ └┘
220 by rw [of_mul_mk, mul_one]
id └───────┘ └─────┘
src └──┘└───────┘└┘└─────┘└─
typ └──┘└───────┘└┘└─────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └────────────┘└───────┘┴└
221
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
222 @[simp, to_additive] lemma mk_mul_cancel_right (x : X) (y : Y) :
id ┴ ┴
typ ┴ ┴
doc └──┘ └─────────┘
223 mk (x * y) y = of Y x :=
id └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
src └┘ ┴ ┴ └┘
typ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
doc └┘ └┘
224 by rw [mk_eq_mul_mk_one, (of Y).map_mul, mul_assoc, ←mk_eq_mul_mk_one, mk_self', mul_one]
id └──────────────┘ └┘ ┴ └───────┘ └──────────────┘ └──────┘ └─────┘
src └──┘└──────────────┘└┘ └┘┴ └─────────┘└───────┘└─┘└──────────────┘└┘└──────┘└┘└─────┘└─
typ └──┘└──────────────┘└┘ └┘┴┴└─────────┘└───────┘└─┘└──────────────┘└┘└──────┘└┘└─────┘└─
doc └──┘ └┘ └┘┴ └─────────┘ └─┘ └┘ └┘ └─
txt └──┘ └┘ ┴ └─────────┘ └─┘ └┘ └┘ └─
par └──┘ └┘ ┴ └─────────┘ └─┘ └┘ └┘ └─
pid └┘ └┘ ┴ └─────────┘ └─┘ └┘ └┘ ┴└
st └───────────────────┘└─────────────┘└──────────┘└─────────────────┘└────────┘└───────┘┴└
225
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
226 @[simp, to_additive] lemma mk_mul_cancel_left (x : X) (y : Y) :
id ┴ ┴
typ ┴ ┴
doc └──┘ └─────────┘
227 mk ((y : X) * x) y = of Y x :=
id └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
src └┘ ┴ ┴ └┘
typ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
doc └┘ └┘
228 by rw [mul_comm, mk_mul_cancel_right]
id └──────┘ └─────────────────┘
src └──┘└──────┘└┘└─────────────────┘└─
typ └──┘└──────┘└┘└─────────────────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └───────────┘└───────────────────┘┴└
229
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
230 /-- Natural homomorphism sending `y ∈ Y`, `Y` a submonoid of a `comm_monoid` `X`, to the units of
231 the localization of `X` at `Y`. -/
232 def to_units (Y : submonoid X) : Y →* units (monoid_localization X Y) :=
id └───────┘ ┴ ┴ └┘ └───┘ └─────────────────┘ ┴ ┴
src └───────┘ └┘ └───┘ └─────────────────┘
typ └───────┘ ┴ ┴ └┘ └───┘ └─────────────────┘ ┴ ┴
doc └───────┘ └┘ └─────────────────┘
233 ⟨λ y, ⟨mk y 1, mk 1 y, by simp, by simp⟩, by simp; refl,
id ┴ └┘ ┴ └┘ ┴
src └┘ └┘ └──┘ └──┘ └──┘ └──┘
typ ┴ └┘ ┴ └┘ ┴ └──┘ └──┘ └──┘ └──┘
doc └┘ └┘ └──┘ └──┘ └──┘ └──┘
txt └──┘ └──┘ └──┘ └──┘
par └──┘ └──┘ └──┘ └──┘
st └───┘ └───┘ └─────────┘
234 λ _ _, by ext; convert (of Y).map_mul _ _⟩
id ┴ ┴ └┘ ┴
src └─┘ └──────┘ └┘┴ └───────────┘
typ ┴ ┴ └─┘ └──────┘ └┘┴┴└───────────┘
doc └─┘ └──────┘ └┘┴ └───────────┘
txt └─┘ └──────┘ ┴ └───────────┘
par └─┘ └──────┘ ┴ └───────────┘
pid ┴ ┴ └───────────┘
st └──────────────────────────────┘
235
236 @[simp] lemma to_units_mk (y) : (to_units Y y : monoid_localization X Y) = mk y 1 := rfl
id └──────┘ ┴ ┴ └─────────────────┘ ┴ ┴ ┴ └┘ ┴ └─┘
src └──────┘ └─────────────────┘ ┴ └┘ └─┘
typ └──────┘ ┴ ┴ └─────────────────┘ ┴ ┴ ┴ └┘ ┴ └─┘
doc └──┘ └──────┘ └─────────────────┘ └┘
237
238 @[simp] lemma mk_is_unit (y : Y) : is_unit (mk (y : X) (1 : Y)) :=
id ┴ └─────┘ └┘ ┴ ┴ ┴
src └─────┘ └┘
typ ┴ └─────┘ └┘ ┴ ┴ ┴
doc └──┘ └─────┘ └┘
239 is_unit_unit $ to_units Y y
id └──────────┘ └──────┘ ┴ ┴
src └──────────┘ └──────┘
typ └──────────┘ └──────┘ ┴ ┴
doc └──────┘
240
241 @[simp] lemma mk_is_unit' (x) (hx : x ∈ Y) : is_unit (mk x (1 : Y)) :=
id ┴ ┴ ┴ └─────┘ └┘ ┴ ┴
src ┴ └─────┘ └┘
typ ┴ ┴ ┴ └─────┘ └┘ ┴ ┴
doc └──┘ └─────┘ └┘
242 is_unit_unit $ to_units Y ⟨x, hx⟩
id └──────────┘ └──────┘ ┴ ┴ └┘
src └──────────┘ └──────┘
typ └──────────┘ └──────┘ ┴ ┴ └┘
doc └──────┘
243
244 lemma to_units_inv (y) : mk 1 y = ↑(to_units Y y)⁻¹ := rfl
id └┘ ┴ ┴ ┴ └──────┘ ┴ ┴ └┘ └─┘
src └┘ ┴ ┴ └──────┘ └┘ └─┘
typ └┘ ┴ ┴ ┴ └──────┘ ┴ ┴ └┘ └─┘
doc └┘ └──────┘
245
246 @[simp] lemma of_is_unit (y : Y) : is_unit (of Y y) :=
id ┴ └─────┘ └┘ ┴ ┴
src └─────┘ └┘
typ ┴ └─────┘ └┘ ┴ ┴
doc └──┘ └─────┘ └┘
247 is_unit_unit $ to_units Y y
id └──────────┘ └──────┘ ┴ ┴
src └──────────┘ └──────┘
typ └──────────┘ └──────┘ ┴ ┴
doc └──────┘
248
249 @[simp] lemma of_is_unit' (x) (hx : x ∈ Y) : is_unit (of Y x) :=
id ┴ ┴ ┴ └─────┘ └┘ ┴ ┴
src ┴ └─────┘ └┘
typ ┴ ┴ ┴ └─────┘ └┘ ┴ ┴
doc └──┘ └─────┘ └┘
250 is_unit_unit $ to_units Y ⟨x, hx⟩
id └──────────┘ └──────┘ ┴ ┴ └┘
src └──────────┘ └──────┘
typ └──────────┘ └──────┘ ┴ ┴ └┘
doc └──────┘
251
252 lemma to_units_map_inv (g : monoid_localization X Y →* Z) (y) :
id └─────────────────┘ ┴ ┴ └┘ ┴
src └─────────────────┘ └┘
typ └─────────────────┘ ┴ ┴ └┘ ┴
doc └─────────────────┘ └┘
253 g ↑(to_units Y y)⁻¹ = ↑(units.map g (to_units Y y))⁻¹ :=
id ┴ ┴ └──────┘ ┴ ┴ └┘ ┴ ┴ └───────┘ ┴ └──────┘ ┴ ┴ └┘
src ┴ └──────┘ └┘ ┴ ┴ └───────┘ └──────┘ └┘
typ ┴ ┴ └──────┘ ┴ ┴ └┘ ┴ ┴ └───────┘ ┴ └──────┘ ┴ ┴ └┘
doc └──────┘ └──────┘
254 by rw [←units.coe_map, (units.map g).map_inv]
id └───────────┘ └───────┘ ┴
src └───┘└───────────┘└┘ └───────┘┴ └──────────
typ └───┘└───────────┘└┘ └───────┘┴┴└──────────
doc └───┘ └┘ ┴ └──────────
txt └───┘ └┘ ┴ └──────────
par └───┘ └┘ ┴ └──────────
pid └─┘ └┘ ┴ └────────┘└
st └─────────────────┘└────────────────────┘└┘└
255
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
256 lemma mk_eq (x y) : mk x y = of Y x * ↑(to_units Y y)⁻¹ :=
id └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └┘
src └┘ ┴ └┘ ┴ ┴ └──────┘ └┘
typ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └┘
doc └┘ └┘ └──────┘
257 by rw ←to_units_inv; simp only [of_eq_mk, mk_mul_mk, mul_one, one_mul]
id └──────────┘ └──────┘ └───────┘ └─────┘ └─────┘
src └──┘└──────────┘ └─────────┘└──────┘└┘└───────┘└┘└─────┘└┘└─────┘└─
typ └──┘└──────────┘ └─────────┘└──────┘└┘└───────┘└┘└─────┘└┘└─────┘└─
doc └──┘ └─────────┘ └┘ └┘ └┘ └─
txt └──┘ └─────────┘ └┘ └┘ └┘ └─
par └──┘ └─────────┘ └┘ └┘ └┘ └─
pid └┘ ┴└──┘└┘ └┘ └┘ └┘ ┴└
st └────────────────────────────────────────────────────────────────────
258
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
259 variables {f : X →* Z}
id └┘
src └┘
typ └┘
doc └┘
260
261 lemma is_unit_of_of_comp {W : submonoid Z} (hf : ∀ y : Y, f y ∈ W) {y : Y} :
id └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴
typ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────┘
262 is_unit (of W (f y)) :=
id └─────┘ └┘ ┴ ┴ ┴
src └─────┘ └┘
typ └─────┘ └┘ ┴ ┴ ┴
doc └─────┘ └┘
263 ⟨to_units W ⟨f y, hf y⟩, rfl⟩
id └──────┘ ┴ ┴ ┴ └┘ ┴ └─┘
src └──────┘ └─┘
typ └──────┘ ┴ ┴ ┴ └┘ ┴ └─┘
doc └──────┘
264
265 variables {g : Y → units Z}
id └───┘
src └───┘
typ └───┘
266
267 lemma units_restrict_mul (H : ∀ y : Y, f y = g y) {x y} : g (x * y) = g x * g y :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
268 by ext; rw [units.coe_mul, ←H _, ←H _, ←H _]; apply f.map_mul
id └───────────┘ ┴ ┴ ┴
src └─┘ └──┘└───────────┘└─┘ └───┘ └───┘ └─┘ └────┘ └
typ └─┘ └──┘└───────────┘└─┘┴└───┘┴└───┘┴└─┘ └────┘ └
doc └─┘ └──┘ └─┘ └───┘ └───┘ └─┘ └────┘ └
txt └─┘ └──┘ └─┘ └───┘ └───┘ └─┘ └────┘ └
par └─┘ └──┘ └─┘ └───┘ └───┘ └─┘ └────┘ └
pid └┘ └─┘ └───┘ └───┘ └─┘ ┴ └
st └────────┘└───────────┘└────┘└────┘└────┘┴└─────────────────
269
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
270 variables (f)
271
272 /-- Given a `comm_monoid` homomorphism `f : X → Z` mapping elements of a submonoid `Y` to
273 invertible elements of `Z`, the induced homomorphism from `Y` to the units of `Z`. -/
274 def units_restrict (H : ∀ y : Y, f y = g y) : Y →* units Z :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └───┘ ┴
src ┴ └┘ └───┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └───┘ ┴
doc └┘
275 ⟨g, units.ext $ (H 1) ▸ f.map_one, λ _ _, units_restrict_mul H⟩
id ┴ └───────┘ ┴ ┴ ┴└──────┘ ┴ ┴ └────────────────┘ ┴
src └───────┘ ┴ └──────┘ └────────────────┘
typ ┴ └───────┘ ┴ ┴ ┴└──────┘ ┴ ┴ └────────────────┘ ┴
doc └──────┘
276
277 variables (g)
278
279 /-- Given a `comm_monoid` homomorphism `f : X → Z` mapping elements of a submonoid `Y` to
280 invertible elements of `Z`, the homomorphism from `X × Y` to `Z` sending `(x, y)` to
281 `f(x) * f(y)⁻¹`; this induces a homomorphism from the localization of `X` at `Y`
282 (constructive version). -/
283 def aux (H : ∀ y : Y, f y = g y) : X × Y →* Z :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
src ┴ ┴ └┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
doc └┘
284 (f.comp prod.monoid_hom.fst).mul $
id ┴└───┘ └─────────────────┘ └─┘
src └───┘ └─────────────────┘ └─┘
typ ┴└───┘ └─────────────────┘ └─┘
doc └───┘ └─────────────────┘ └─┘
285 (units.coe_hom Z).comp ((units_restrict f H).comp prod.monoid_hom.snd).inv
id └───────────┘ ┴ └──┘ └────────────┘ ┴ ┴ └──┘ └─────────────────┘ └─┘
src └───────────┘ └──┘ └────────────┘ └──┘ └─────────────────┘ └─┘
typ └───────────┘ ┴ └──┘ └────────────┘ ┴ ┴ └──┘ └─────────────────┘ └─┘
doc └───────────┘ └──┘ └────────────┘ └──┘ └─────────────────┘ └─┘
286
287 variables {g}
288
289 /-- Given a `comm_monoid` homomorphism `f : X → Z` mapping elements of a submonoid `Y` to
290 invertible elements of `Z`, the homomorphism from `X × Y` to `Z` sending `(x, y)` to
291 `f(x) * f(y)⁻¹` is constant on the equivalence classes of the localization of `X` at `Y`. -/
292 lemma r_le_ker_aux (H : ∀ y : Y, f y = g y) :
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
293 Y.r ≤ con.ker (aux f g H) :=
id ┴└┘ ┴ └─────┘ └─┘ ┴ ┴ ┴
src └┘ ┴ └─────┘ └─┘
typ ┴└┘ ┴ └─────┘ └─┘ ┴ ┴ ┴
doc └┘ └─────┘ └─┘
294 con.Inf_le _ _ (λ y, show f (1 : Y) * ↑(g 1)⁻¹ = f y * ↑(g y)⁻¹, by
id └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
src └────────┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘
typ └────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
doc └────────┘
st └
295 rw [H 1, H y]; simp [units.mul_inv])
id ┴ ┴ ┴ └───────────┘
src └──┘ └──┘ ┴ ┴ └────┘└───────────┘┴
typ └──┘┴└──┘┴┴┴┴ └────┘└───────────┘┴
doc └──┘ └──┘ ┴ ┴ └────┘ ┴
txt └──┘ └──┘ ┴ ┴ └────┘ ┴
par └──┘ └──┘ ┴ ┴ └────┘ ┴
pid └┘ └──┘ ┴ ┴ ┴┴ ┴
st ───────┘└────┘┴└────────────────────┘
296
297 /-- Given a `comm_monoid` homomorphism `f : X → Z` mapping elements of a submonoid `Y` to
298 invertible elements of `Z`, the homomorphism from the localization of `X` at `Y` sending
299 `⟦(x, y)⟧` to `f(x) * f(y)⁻¹`. -/
300 def lift' (g : Y → units Z) (H : ∀ y : Y, f y = g y) : monoid_localization X Y →* Z :=
id ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘ ┴ ┴ └┘ ┴
src └───┘ ┴ └─────────────────┘ └┘
typ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────────┘ ┴ ┴ └┘ ┴
doc └─────────────────┘ └┘
301 Y.r.lift (aux f g H) $ r_le_ker_aux f H
id ┴└┘└───┘ └─┘ ┴ ┴ ┴ └──────────┘ ┴ ┴
src └┘└───┘ └─┘ └──────────┘
typ ┴└┘└───┘ └─┘ ┴ ┴ ┴ └──────────┘ ┴ ┴
doc └┘└───┘ └─┘ └──────────┘
302
303 /-- Given a `comm_monoid` homomorphism `f : X → Z` mapping elements of a submonoid `Y` to
304 invertible elements of `Z`, the homomorphism from the localization of `X` at `Y` sending
305 `⟦(x, y)⟧` to `f(x) * f(y)⁻¹`, where `f(y)⁻¹` is chosen nonconstructively. -/
306 noncomputable def lift (H : ∀ y : Y, is_unit (f y)) : monoid_localization X Y →* Z :=
id ┴ └─────┘ ┴ ┴ └─────────────────┘ ┴ ┴ └┘ ┴
src └─────┘ └─────────────────┘ └┘
typ ┴ └─────┘ ┴ ┴ └─────────────────┘ ┴ ┴ └┘ ┴
doc └─────┘ └─────────────────┘ └┘
307 lift' f _ $ λ _, classical.some_spec $ H _
id └───┘ ┴ ┴ └─────────────────┘ ┴
src └───┘ └─────────────────┘
typ └───┘ ┴ ┴ └─────────────────┘ ┴
doc └───┘
308
309 variables {f}
310
311 @[simp] lemma lift'_mk (H : ∀ y : Y, f y = g y) (x y) :
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
312 lift' f _ H (mk x y) = f x * ↑(g y)⁻¹ := rfl
id └───┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └─┘
src └───┘ └┘ ┴ ┴ ┴ └┘ └─┘
typ └───┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └─┘
doc └───┘ └┘
313
314 @[simp] lemma lift_mk (H : ∀ y : Y, is_unit (f y)) (x y) :
id ┴ └─────┘ ┴ ┴
src └─────┘
typ ┴ └─────┘ ┴ ┴
doc └──┘ └─────┘
315 lift f H (mk x y) = f x * ↑(classical.some (H y))⁻¹ := rfl
id └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴ └┘ └─┘
src └──┘ └┘ ┴ ┴ ┴ └────────────┘ └┘ └─┘
typ └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴ └┘ └─┘
doc └──┘ └┘
316
317 @[simp] lemma lift'_of (H : ∀ y : Y, f y = g y) (x : X) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
318 lift' f _ H (of Y x) = f x :=
id └───┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
src └───┘ └┘ ┴
typ └───┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
doc └───┘ └┘
319 show f x * ↑(g 1)⁻¹ = _, by
id ┴ ┴ ┴ ┴ ┴ └┘ ┴
src ┴ ┴ └┘ ┴
typ ┴ ┴ ┴ ┴ ┴ └┘ ┴
st └
320 rw [inv_eq_one.2 (show g 1 = 1, from units.ext $ (H 1) ▸ f.map_one), units.coe_one, mul_one]
id └────────┘ ┴ ┴ └───────┘ ┴ ┴ └───────┘ └───────────┘ └─────┘
src └──┘└────────┘└─┘ ┴ └─┘┴└───────┘└───────┘┴ ┴ └──┘┴┴└───────┘└─┘└───────────┘└┘└─────┘└─
typ └──┘└────────┘└─┘ ┴┴└─┘┴└───────┘└───────┘┴ ┴ ┴└──┘┴┴└───────┘└─┘└───────────┘└┘└─────┘└─
doc └──┘ └─┘ ┴ └─┘ └───────┘ ┴ ┴ └──┘ ┴└───────┘└─┘ └┘ └─
txt └──┘ └─┘ ┴ └─┘ └───────┘ ┴ ┴ └──┘ ┴ └─┘ └┘ └─
par └──┘ └─┘ ┴ └─┘ └───────┘ ┴ ┴ └──┘ ┴ └─┘ └┘ └─
pid └┘ └─┘ ┴ └─┘ └───────┘ ┴ ┴ └──┘ ┴ └─┘ └┘ ┴└
st ────────────────────────────────────────────────────────────────────┘└─────────────┘└───────┘┴└
321
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
322 @[simp] lemma lift_of (H : ∀ y : Y, is_unit (f y)) (x : X) :
id ┴ └─────┘ ┴ ┴ ┴
src └─────┘
typ ┴ └─────┘ ┴ ┴ ┴
doc └──┘ └─────┘
323 lift f H (of Y x) = f x := lift'_of _ _
id └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └──────┘
src └──┘ └┘ ┴ └──────┘
typ └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └──────┘
doc └──┘ └┘
324
325 lemma lift'_eq_iff (H : ∀ y : Y, f y = g y) {x y : X × Y} :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
326 lift' f g H (mk x.1 x.2) = lift' f g H (mk y.1 y.2) ↔ f (y.2 * x.1) = f (y.1 * x.2) :=
id └───┘ ┴ ┴ ┴ └┘ ┴┴ ┴┴ ┴ └───┘ ┴ ┴ ┴ └┘ ┴┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴┴
src └───┘ └┘ ┴ ┴ ┴ └───┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └───┘ ┴ ┴ ┴ └┘ ┴┴ ┴┴ ┴ └───┘ ┴ ┴ ┴ └┘ ┴┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴┴
doc └───┘ └┘ └───┘ └┘
327 by rw [lift'_mk, lift'_mk, units.eq_mul_inv_iff_mul_eq, mul_comm, ←mul_assoc,
id └──────┘ └──────┘ └─────────────────────────┘ └──────┘ └───────┘
src └──┘└──────┘└┘└──────┘└┘└─────────────────────────┘└┘└──────┘└─┘└───────┘└─
typ └──┘└──────┘└┘└──────┘└┘└─────────────────────────┘└┘└──────┘└─┘└───────┘└─
doc └──┘ └┘ └┘ └┘ └─┘ └─
txt └──┘ └┘ └┘ └┘ └─┘ └─
par └──┘ └┘ └┘ └┘ └─┘ └─
pid └┘ └┘ └┘ └┘ └─┘ └─
st └───────────┘└────────┘└───────────────────────────┘└────────┘└──────────┘└─
328 units.mul_inv_eq_iff_eq_mul, ←H _, ←H _, ←f.map_mul, ←f.map_mul]
id └─────────────────────────┘ ┴ ┴
src ──────┘└─────────────────────────┘└─┘ └───┘ └───┘ └─┘ └─
typ ──────┘└─────────────────────────┘└─┘┴└───┘┴└───┘└───────┘└─┘└───────┘└─
doc ──────┘ └─┘ └───┘ └───┘ └─┘ └─
txt ──────┘ └─┘ └───┘ └───┘ └─┘ └─
par ──────┘ └─┘ └───┘ └───┘ └─┘ └─
pid ──────┘ └─┘ └───┘ └───┘ └─┘ ┴└
st ─────────────────────────────────┘└────┘└────┘└──────────┘└──────────┘┴└
329
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
330 lemma lift_eq_iff (H : ∀ y : Y, is_unit (f y)) {x y : X × Y} :
id ┴ └─────┘ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴
typ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴
doc └─────┘
331 lift f H (mk x.1 x.2) = lift f H (mk y.1 y.2) ↔ f (y.2 * x.1) = f (y.1 * x.2) :=
id └──┘ ┴ ┴ └┘ ┴┴ ┴┴ ┴ └──┘ ┴ ┴ └┘ ┴┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴┴
src └──┘ └┘ ┴ ┴ ┴ └──┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └──┘ ┴ ┴ └┘ ┴┴ ┴┴ ┴ └──┘ ┴ ┴ └┘ ┴┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴┴
doc └──┘ └┘ └──┘ └┘
332 lift'_eq_iff _
id └──────────┘
src └──────────┘
typ └──────────┘
333
334 lemma mk_eq_iff_of_eq {x y : X × Y} :
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
335 mk x.1 x.2 = mk y.1 y.2 ↔ of Y (y.2 * x.1) = of Y (y.1 * x.2) :=
id └┘ ┴┴ ┴┴ ┴ └┘ ┴┴ ┴┴ ┴ └┘ ┴ ┴┴ ┴ ┴┴ ┴ └┘ ┴ ┴┴ ┴ ┴┴
src └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴
typ └┘ ┴┴ ┴┴ ┴ └┘ ┴┴ ┴┴ ┴ └┘ ┴ ┴┴ ┴ ┴┴ ┴ └┘ ┴ ┴┴ ┴ ┴┴
doc └┘ └┘ └┘ └┘
336 by rw [mk_eq, mk_eq, ←lift'_mk, ←lift'_mk];
id └───┘ └───┘ └──────┘ └──────┘
src └──┘└───┘└┘└───┘└─┘└──────┘└─┘└──────┘┴
typ └──┘└───┘└┘└───┘└─┘└──────┘└─┘└──────┘┴
doc └──┘ └┘ └─┘ └─┘ ┴
txt └──┘ └┘ └─┘ └─┘ ┴
par └──┘ └┘ └─┘ └─┘ ┴
pid └┘ └┘ └─┘ └─┘ ┴
st └────────┘└─────┘└─────────┘└─────────┘┴└─
337 exact lift'_eq_iff (λ (w : Y), rfl)
id └──────────┘ ┴ └─┘
src └────┘└──────────┘┴ └────┘ └─┘└─┘└─
typ └────┘└──────────┘┴ └────┘┴└─┘└─┘└─
doc └────┘ ┴ └────┘ └─┘ └─
txt └────┘ ┴ └────┘ └─┘ └─
par └────┘ ┴ └────┘ └─┘ └─
pid ┴ ┴ └────┘ └─┘ ┴└
st ──────────────────────────────────────
338
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
339 lemma lift'_comp_of (H : ∀ y : Y, f y = g y) :
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
340 (lift' f _ H).comp (of Y) = f :=
id └───┘ ┴ ┴ └──┘ └┘ ┴ ┴ ┴
src └───┘ └──┘ └┘ ┴
typ └───┘ ┴ ┴ └──┘ └┘ ┴ ┴ ┴
doc └───┘ └──┘ └┘
341 by ext; exact lift'_of H _
id └──────┘ ┴
src └─┘ └────┘└──────┘┴ └──
typ └─┘ └────┘└──────┘┴┴└──
doc └─┘ └────┘ ┴ └──
txt └─┘ └────┘ ┴ └──
par └─┘ └────┘ ┴ └──
pid ┴ ┴ └┘└
st └────────────────────────
342
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
343 @[simp] lemma lift_comp_of (H : ∀ y : Y, is_unit (f y)) :
id ┴ └─────┘ ┴ ┴
src └─────┘
typ ┴ └─────┘ ┴ ┴
doc └──┘ └─────┘
344 (lift f H).comp (of Y) = f := lift'_comp_of _
id └──┘ ┴ ┴ └──┘ └┘ ┴ ┴ ┴ └───────────┘
src └──┘ └──┘ └┘ ┴ └───────────┘
typ └──┘ ┴ ┴ └──┘ └┘ ┴ ┴ ┴ └───────────┘
doc └──┘ └──┘ └┘
345
346 @[simp] lemma lift'_apply_of (f' : monoid_localization X Y →* Z)
id └─────────────────┘ ┴ ┴ └┘ ┴
src └─────────────────┘ └┘
typ └─────────────────┘ ┴ ┴ └┘ ┴
doc └──┘ └─────────────────┘ └┘
347 (H : ∀ y : Y, f'.comp (of Y) y = g y) : lift' (f'.comp (of Y)) _ H = f' :=
id ┴ └┘└───┘ └┘ ┴ ┴ ┴ ┴ ┴ └───┘ └┘└───┘ └┘ ┴ ┴ ┴ └┘
src └───┘ └┘ ┴ └───┘ └───┘ └┘ ┴
typ ┴ └┘└───┘ └┘ ┴ ┴ ┴ ┴ ┴ └───┘ └┘└───┘ └┘ ┴ ┴ ┴ └┘
doc └───┘ └┘ └───┘ └───┘ └┘
348 begin
st └─────
349 ext x,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ──────┘└─
350 apply induction_on x,
id └──────────┘ ┴
src └────┘└──────────┘┴
typ └────┘└──────────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────────────────┘└─
351 intros,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
st ───────┘└─
352 rw [lift'_mk, ←units.mul_right_inj (g y.2), mul_assoc, units.inv_mul, ←H y.2,
id └──────┘ └─────────────────┘ ┴ ┴ └───────┘ └───────────┘ ┴ ┴
src └──┘└──────┘└─┘└─────────────────┘┴ ┴ └───┘└───────┘└┘└───────────┘└─┘ ┴ └───
typ └──┘└──────┘└─┘└─────────────────┘┴ ┴┴┴└───┘└───────┘└┘└───────────┘└─┘┴┴┴└───
doc └──┘ └─┘ ┴ ┴ └───┘ └┘ └─┘ ┴ └───
txt └──┘ └─┘ ┴ ┴ └───┘ └┘ └─┘ ┴ └───
par └──┘ └─┘ ┴ ┴ └───┘ └┘ └─┘ ┴ └───
pid └┘ └─┘ ┴ ┴ └───┘ └┘ └─┘ ┴ └───
st ─────────────┘└────────────────────────────┘└─────────┘└─────────────┘└────┘└───
353 mul_one, mk_eq_mul_mk_one],
id └─────┘ └──────────────┘
src ─────┘└─────┘└┘└──────────────┘┴
typ ─────┘└─────┘└┘└──────────────┘┴
doc ─────┘ └┘ ┴
txt ─────┘ └┘ ┴
par ─────┘ └┘ ┴
pid ─────┘ └┘ ┴
st ────────────┘└────────────────┘└──
354 show f' _ = f' (mk _ _ * _) * f' (mk _ _),
id ┴ ┴ └┘ └┘
src └───┘ └─┘┴┴ ┴ └───┘┴└──┘ ┴ ┴ └┘└───┘
typ └───┘ └─┘┴┴ ┴ └───┘┴└──┘ ┴└┘┴ └┘└───┘
doc └───┘ └─┘ ┴ ┴ └───┘ └──┘ ┴ ┴ └┘└───┘
txt └───┘ └─┘ ┴ ┴ └───┘ └──┘ ┴ ┴ └───┘
par └───┘ └─┘ ┴ ┴ └───┘ └──┘ ┴ ┴ └───┘
pid └───┘ └─┘ ┴ ┴ └───┘ └──┘ ┴ ┴ └───┘
st ──────────────────────────────────────────┘└─
355 rw [←f'.map_mul, mk_mul_mk, mk_mul_mk],
id └───────┘ └───────┘
src └───┘ └┘└───────┘└┘└───────┘┴
typ └───┘└────────┘└┘└───────┘└┘└───────┘┴
doc └───┘ └┘ └┘ ┴
txt └───┘ └┘ └┘ ┴
par └───┘ └┘ └┘ ┴
pid └─┘ └┘ └┘ ┴
st ────────────────┘└─────────┘└─────────┘└──
356 simp only [mul_one, mk_mul_cancel_right, one_mul],
id └─────┘ └─────────────────┘ └─────┘
src └─────────┘└─────┘└┘└─────────────────┘└┘└─────┘┴
typ └─────────┘└─────┘└┘└─────────────────┘└┘└─────┘┴
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st ──────────────────────────────────────────────────┘└─
357 end
st ──┘
358
359 @[simp] lemma lift_apply_of (g : monoid_localization X Y →* Z) :
id └─────────────────┘ ┴ ┴ └┘ ┴
src └─────────────────┘ └┘
typ └─────────────────┘ ┴ ┴ └┘ ┴
doc └──┘ └─────────────────┘ └┘
360 lift (g.comp $ of Y) (λ y, is_unit_unit $ units.map g $ to_units Y y) = g :=
id └──┘ ┴└───┘ └┘ ┴ ┴ └──────────┘ └───────┘ ┴ └──────┘ ┴ ┴ ┴ ┴
src └──┘ └───┘ └┘ └──────────┘ └───────┘ └──────┘ ┴
typ └──┘ ┴└───┘ └┘ ┴ ┴ └──────────┘ └───────┘ ┴ └──────┘ ┴ ┴ ┴ ┴
doc └──┘ └───┘ └┘ └──────┘
361 lift'_apply_of _ _
id └────────────┘
src └────────────┘
typ └────────────┘
362
363 lemma funext (f g : monoid_localization X Y →* Z)
id └─────────────────┘ ┴ ┴ └┘ ┴
src └─────────────────┘ └┘
typ └─────────────────┘ ┴ ┴ └┘ ┴
doc └─────────────────┘ └┘
364 (h : ∀ a, f.comp (of Y) a = g.comp (of Y) a) : f = g :=
id ┴ ┴└───┘ └┘ ┴ ┴ ┴ ┴└───┘ └┘ ┴ ┴ ┴ ┴ ┴
src └───┘ └┘ ┴ └───┘ └┘ ┴
typ ┴ ┴└───┘ └┘ ┴ ┴ ┴ ┴└───┘ └┘ ┴ ┴ ┴ ┴ ┴
doc └───┘ └┘ └───┘ └┘
365 begin
st └─────
366 rw [←lift_apply_of f, ←lift_apply_of g],
id └───────────┘ ┴ └───────────┘ ┴
src └───┘└───────────┘┴ └─┘└───────────┘┴ ┴
typ └───┘└───────────┘┴┴└─┘└───────────┘┴┴┴
doc └───┘ ┴ └─┘ ┴ ┴
txt └───┘ ┴ └─┘ ┴ ┴
par └───┘ ┴ └─┘ ┴ ┴
pid └─┘ ┴ └─┘ ┴ ┴
st ─────────────────────┘└────────────────┘└──
367 congr' 1,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid ┴┴
st ─────────┘└─
368 ext,
src └─┘
typ └─┘
doc └─┘
txt └─┘
par └─┘
st ────┘└─
369 convert h x,
id ┴ ┴
src └──────┘ ┴
typ └──────┘┴┴┴
doc └──────┘ ┴
txt └──────┘ ┴
par └──────┘ ┴
pid ┴ ┴
st ────────────┘└─
370 end
st ──┘
371
372 variables {W : submonoid Z} (f)
id └───────┘
src └───────┘
typ └───────┘
doc └───────┘
373
374 /-- Given a `comm_monoid` homomorphism `f : X → Z` where for submonoids `Y ⊆ X, W ⊆ Z` we have
375 `f(Y) ⊆ W`, the monoid homomorphism from the localization of `X` at `Y` to the localization of
376 `Z` at `W` induced by the natural map from `Z` to the localization of `Z` at
377 `W` composed with `f`. -/
378 def map (hf : ∀ y : Y, f y ∈ W) : monoid_localization X Y →* monoid_localization Z W :=
id ┴ ┴ ┴ ┴ ┴ └─────────────────┘ ┴ ┴ └┘ └─────────────────┘ ┴ ┴
src ┴ └─────────────────┘ └┘ └─────────────────┘
typ ┴ ┴ ┴ ┴ ┴ └─────────────────┘ ┴ ┴ └┘ └─────────────────┘ ┴ ┴
doc └─────────────────┘ └┘ └─────────────────┘
379 lift' ((of W).comp f) ((to_units W).comp $ (f.comp Y.subtype).subtype_mk W hf) $ λ y, rfl
id └───┘ └┘ ┴ └──┘ ┴ └──────┘ ┴ └──┘ ┴└───┘ ┴└──────┘ └────────┘ ┴ └┘ ┴ └─┘
src └───┘ └┘ └──┘ └──────┘ └──┘ └───┘ └──────┘ └────────┘ └─┘
typ └───┘ └┘ ┴ └──┘ ┴ └──────┘ ┴ └──┘ ┴└───┘ ┴└──────┘ └────────┘ ┴ └┘ ┴ └─┘
doc └───┘ └┘ └──┘ └──────┘ └──┘ └───┘ └──────┘ └────────┘
380
381 variables {f}
382
383 lemma map_eq (hf : ∀ y : Y, f y ∈ W) :
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
384 map f hf = lift ((of W).comp f) (λ y, ⟨to_units W ⟨f y, hf y⟩, rfl⟩) :=
id └─┘ ┴ └┘ ┴ └──┘ └┘ ┴ └──┘ ┴ ┴ └──────┘ ┴ ┴ ┴ └┘ ┴ └─┘
src └─┘ ┴ └──┘ └┘ └──┘ └──────┘ └─┘
typ └─┘ ┴ └┘ ┴ └──┘ └┘ ┴ └──┘ ┴ ┴ └──────┘ ┴ ┴ ┴ └┘ ┴ └─┘
doc └─┘ └──┘ └┘ └──┘ └──────┘
385 by rw map; congr; ext; erw ←classical.some_spec (is_unit_of_of_comp hf); refl
id └─┘ └─────────────────┘ └────────────────┘ └┘
src └─┘└─┘ └───┘ └─┘ └───┘└─────────────────┘┴ └────────────────┘┴ ┴ └────
typ └─┘└─┘ └───┘ └─┘ └───┘└─────────────────┘┴ └────────────────┘┴└┘┴ └────
doc └─┘└─┘ └─┘ └───┘ ┴ ┴ ┴ └────
txt └─┘ └───┘ └─┘ └───┘ ┴ ┴ ┴ └────
par └─┘ └───┘ └─┘ └───┘ ┴ ┴ ┴ └────
pid ┴ └┘ ┴ ┴ ┴ └
st └───────────────────────────────────────────────────────────────────────────
386
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
387 @[simp] lemma map_of (hf : ∀ y : Y, f y ∈ W) (x) :
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
doc └──┘
388 map f hf (of Y x) = of W (f x) := lift'_of _ _
id └─┘ ┴ └┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──────┘
src └─┘ └┘ ┴ └┘ └──────┘
typ └─┘ ┴ └┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──────┘
doc └─┘ └┘ └┘
389
390 @[simp] lemma map_comp_of (hf : ∀ y : Y, f y ∈ W) :
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
doc └──┘
391 (map f hf).comp (of Y) = (of W).comp f := lift'_comp_of _
id └─┘ ┴ └┘ └──┘ └┘ ┴ ┴ └┘ ┴ └──┘ ┴ └───────────┘
src └─┘ └──┘ └┘ ┴ └┘ └──┘ └───────────┘
typ └─┘ ┴ └┘ └──┘ └┘ ┴ ┴ └┘ ┴ └──┘ ┴ └───────────┘
doc └─┘ └──┘ └┘ └┘ └──┘
392
393 lemma map_mk (hf : ∀ y : Y, f y ∈ W) (x y) :
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
394 map f hf (mk x y) = mk (f x) ⟨f y, hf y⟩ :=
id └─┘ ┴ └┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴
src └─┘ └┘ ┴ └┘
typ └─┘ ┴ └┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴
doc └─┘ └┘ └┘
395 (lift'_mk _ _ _).trans (mk_eq _ _).symm
id └──────┘ └───┘ └───┘ └──┘
src └──────┘ └───┘ └───┘ └──┘
typ └──────┘ └───┘ └───┘ └──┘
396
397 @[simp] lemma map_id (x : monoid_localization X Y) :
id └─────────────────┘ ┴ ┴
src └─────────────────┘
typ └─────────────────┘ ┴ ┴
doc └──┘ └─────────────────┘
398 map (monoid_hom.id X) (λ (y : Y), y.2) x = x :=
id └─┘ └───────────┘ ┴ ┴ ┴┴ ┴ ┴ ┴
src └─┘ └───────────┘ ┴ ┴
typ └─┘ └───────────┘ ┴ ┴ ┴┴ ┴ ┴ ┴
doc └─┘ └───────────┘
399 induction_on x $ λ ⟨w, z⟩, by rw map_mk; exact congr_arg _ (subtype.eq' rfl)
id └──────────┘ ┴ ┴ └────┘ └───────┘ └─────────┘ └─┘
src └──────────┘ └─┘└────┘ └────┘└───────┘└─┘ └─────────┘┴└─┘└─
typ └──────────┘ ┴ ┴ └─┘└────┘ └────┘└───────┘└─┘ └─────────┘┴└─┘└─
doc └─┘ └────┘ └─┘ ┴ └─
txt └─┘ └────┘ └─┘ ┴ └─
par └─┘ └────┘ └─┘ ┴ └─
pid ┴ ┴ └─┘ ┴ ┴└
st └───────────────────────────────────────────────
400
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
401 lemma map_comp_map {A} [comm_monoid A] {V} {g : Z →* A}
id └─────────┘ ┴ ┴ └┘ ┴
src └─────────┘ └┘
typ └─────────┘ ┴ ┴ └┘ ┴
doc └┘
402 (hf : ∀ y : Y, f y ∈ W) (hg : ∀ w : W, g w ∈ V) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
403 (map g hg).comp (map f hf) = map (g.comp f) (λ y, hg ⟨f y, hf y⟩) :=
id └─┘ ┴ └┘ └──┘ └─┘ ┴ └┘ ┴ └─┘ ┴└───┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └─┘ └──┘ └─┘ ┴ └─┘ └───┘
typ └─┘ ┴ └┘ └──┘ └─┘ ┴ └┘ ┴ └─┘ ┴└───┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
doc └─┘ └──┘ └─┘ └─┘ └───┘
404 funext _ _ $ λ x, by simp only [map_of, monoid_hom.comp_apply]
id └────┘ ┴ └────┘ └───────────────────┘
src └────┘ └─────────┘└────┘└┘└───────────────────┘└─
typ └────┘ ┴ └─────────┘└────┘└┘└───────────────────┘└─
doc └─────────┘ └┘ └─
txt └─────────┘ └┘ └─
par └─────────┘ └┘ └─
pid ┴└──┘└┘ └┘ ┴└
st └──────────────────────────────────────────
405
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
406 lemma map_map {A} [comm_monoid A] {V} {g : Z →* A}
id └─────────┘ ┴ ┴ └┘ ┴
src └─────────┘ └┘
typ └─────────┘ ┴ ┴ └┘ ┴
doc └┘
407 (hf : ∀ y : Y, f y ∈ W) (hg : ∀ w : W, g w ∈ V) (x) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
408 map g hg (map f hf x) = map (g.comp f) (λ y : Y, hg ⟨f y, hf y⟩) x :=
id └─┘ ┴ └┘ └─┘ ┴ └┘ ┴ ┴ └─┘ ┴└───┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴
src └─┘ └─┘ ┴ └─┘ └───┘
typ └─┘ ┴ └┘ └─┘ ┴ └┘ ┴ ┴ └─┘ ┴└───┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴
doc └─┘ └─┘ └─┘ └───┘
409 by rw ←map_comp_map hf hg; refl
id └──────────┘ └┘ └┘
src └──┘└──────────┘┴ ┴ └────
typ └──┘└──────────┘┴└┘┴└┘ └────
doc └──┘ ┴ ┴ └────
txt └──┘ ┴ ┴ └────
par └──┘ ┴ ┴ └────
pid └┘ ┴ ┴ └
st └─────────────────────────────
410
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
411 lemma map_ext (g : X →* Z) (hf : ∀ y : Y, f y ∈ W) (hg : ∀ y : Y, g y ∈ W)
id ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ ┴
typ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘
412 (h : f = g) (x) : map f hf x = map g hg x :=
id ┴ ┴ ┴ └─┘ ┴ └┘ ┴ ┴ └─┘ ┴ └┘ ┴
src ┴ └─┘ ┴ └─┘
typ ┴ ┴ ┴ └─┘ ┴ └┘ ┴ ┴ └─┘ ┴ └┘ ┴
doc └─┘ └─┘
413 induction_on x $ λ _, by {rw [map_mk, map_mk], congr; rw h; refl}
id └──────────┘ ┴ ┴ └────┘ └────┘ ┴
src └──────────┘ └──┘└────┘└┘└────┘┴ └───┘ └─┘ └──┘
typ └──────────┘ ┴ ┴ └──┘└────┘└┘└────┘┴ └───┘ └─┘┴ └──┘
doc └──┘ └┘ ┴ └─┘ └──┘
txt └──┘ └┘ ┴ └───┘ └─┘ └──┘
par └──┘ └┘ ┴ └───┘ └─┘ └──┘
pid └┘ └┘ ┴ ┴
st └──────────┘└──────┘└───────────┘┴└────┘└┘
414
415 end monoid_localization